structure Pfgen_assist = 
struct
  structure P = Proof1

  datatype ttc
    = T_apply of string * ((string * P.pterm) list)
    | T_exact of P.pterm

  val ttclist : ttc list ref = ref []

  fun get_ttcs () = !ttclist

  fun reset_ttcs () = ttclist := []

  fun add_apply str1 plist = ttclist := T_apply(str1, plist) :: (!ttclist)

  fun add_exact pt = ttclist := T_exact(pt)::(!ttclist)

  fun ttc2str speclist emit (T_apply(str1, plist)) = 
      let val str_p = String.concat 
		      (List.map (fn (pname, pt) => 
				    ("("^pname^":="^(LCoqize1.pr_pterm 0 emit speclist pt)^")")) plist)
      in "apply "^str1^" with "^str_p^".\n"
      end
    | ttc2str speclist emit (T_exact(pt)) = 
      let val substr = LCoqize1.pr_pterm 0 emit speclist pt
      in "exact ("^substr^").\n"
      end

  fun ttcs2str speclist emit ttclist = 
      String.concat(List.map (ttc2str speclist emit) ttclist)
  
end